Nuprl Lemma : msystem_wf
11,40
postcript
pdf
msystem{i:l}
Type{i'}
latex
Definitions
t
T
,
System
,
x
:
A
.
B
(
x
)
,
Lemmas
Id
wf
,
msga
wf
,
ma-feasible
wf
origin
Type{i'} Type{i'} T
x:A. B(x)